--- This is to show how the type checker helps detect an infinite loop
--- Adapted for Frege from Mark Jason Dominus talk
--- 'http://perl.plover.com/yak/typing/ Strong Typing and Perl' which uses ML 
module examples.Diverge where


--- split a list 
split ∷ [α] → ([α],[α])
split [] = ([], [])
split (a1:a2:as) = (a1:bs, a2:cs)
    where (bs, cs) = split as
-- when commenting the next line, we get a warning that the
-- case for the singleton list is missing
split singleton = (singleton, [])

--- merge two already sorted lists
merge ∷ Ord α ⇒ [α] → [α] → [α]
merge [] bs = bs
merge (a:as) (b:bs)
    | a <= b    = a : merge as     (b:bs)
    | otherwise = b : merge (a:as) bs
merge (as@_:_) [] = as

{-- 
    sort a list by splitting it into two smaller ones,
    and merging the sorted smaller lists.
    
    When we forget the singleton case (the second equation), 
    the type becomes
    > Ord b => [a] -> [b]
    
    In English, this means: If you pass any list to 'sort',
    it will return a list of any type you want, provided only
    that values of that type can be ordered. In addition,
    it doesn't even care if the values in your list can be ordered.
    
    How is that possible?
    
    It is possible only in two cases:
    - you pass the empty list, and get back a properly typed empty list
    - you pass a non-empty list, but the function does not actually return. 
      Nor will it actually sort the elements in the empty list.
      
    Consider:
    [A] If sort returns, you get a list of arbitrarily typed elements.
    [B] But it can't possibly make a list of arbitrarily typed elements!
    [A] Right! But "ex falso quod libet". Hence, it won't return.
    
    In fact, suppose the evaluation of
    > sort [1]
    The list gets splitted to
    > ([1], [])
    and the result is
    > merge (sort [1]) (sort [])
    And since we now know that
    > sort [1] = merge (sort [1]) (sort [])
    it follows that 
    > merge (sort [1]) (sort []) = merge (merge (sort [1]) (sort [])) (sort [])
    and so forth.
    -}
-- sort :: Ord e => [e] -> [e]
sort [] = []
-- sort [a] = [a]
sort xs = merge (sort as) (sort bs) 
            where (as, bs) = split xs

--- will only type check as long as 'sort' is not fixed
foo :: ([Double], [Bool])
foo = (sort ["how", "so"], sort ["this", "is", "impossible"])